The present invention relates to the determination of the equivalence of two blocks of assignment statements, such as those used in computer programs. The invention provides a method and computer system for carrying out such a determination and also to a computer program product including a computer readable medium having recorded thereon a computer program for performing such determination.
An assignment statement assigns the value of an expression, the right-hand side of the statement, to a variable at the left-hand side of the statement The two sides of the statement are connected by an assignment operator, which in many programming languages (including C and C++) is the equals sign (=). Thus, an example of an assignment statement in a programming language such as C might be x=x+4. The interpretation of the assignment operator (=) in this statement is: take the current value of x (say, 3), add 4 to it and assign the result (7) to x as its new value. This operation is very different from the interpretation of the equal sign in algebra where the statement x=x+4 would be meaningless since in algebra it is used to express an equation and not an assignment. In some programming languages the assignment operator is given the symbol (:=) to avoid confusion between the assignment and equation.
The present invention has for its object, a technique which is specifically relevant to the determination of whether or not two blocks of assignment statements are equivalent. By way of example, such a technique is useful in realising intermediate steps in program verification, program proving, and compiler initiated optimisation of source code. Expressed mathematically, the objective is as follows:
Given, (1) a set of input variables {x1, x2, . . . xm} and a set of output variables {xk, xk+1, . . . xn} with an overlap of variables in the two sets given by the set {xk, xk+1, . . . xm} if k≦m, and (2) two blocks of assignment statements B1 and B2 where B1 comprises the set of assignments {1S1, 1S2, . . . 1SM} and B2 comprises the set of assignments {2S1, 2S2, . . . 2SN}, determine if the two blocks B1 and B2 provide equivalent computations for the output variables.
The term equivalent computation here means that the values for the output variables {xk, xk+1, . . . , xn} produced by B1 are identical to those produced by B2 given the input variables {x1, x2, . . . , xm} even if the sets {1S1, 1S2, . . . 1SM} and {2S1,2S2, . . . , 2SN) are not identical. For example, given the input variables {x1, x2, x3} and output variables {x2, x3, x4}, block B1 might comprise the assignment statements:x5=x1x6=3*x2x3=x1+3*x2x1=x1+x2+x2x2=2x1=x1x4=x5+x6while block B2 comprises the statements:x1=x1+2*x2x3=x1+x2x4=x3x2=2Inspection will reveal that, in either case, the output variables {x2, x3, x4} will produce the same computed values.